<!DOCTYPE html>
<html lang="zh-CN">
<head>
  <meta charset="UTF-8">
<meta name="viewport" content="width=device-width">
<meta name="theme-color" content="#222"><meta name="generator" content="Hexo 6.3.0">

  <link rel="apple-touch-icon" sizes="180x180" href="/blog/images/apple-touch-icon-next.png">
  <link rel="icon" type="image/png" sizes="32x32" href="/blog/images/Horse.png">
  <link rel="icon" type="image/png" sizes="16x16" href="/blog/images/Horse.png">
  <link rel="mask-icon" href="/blog/images/logo.svg" color="#222">

<link rel="stylesheet" href="/blog/css/main.css">



<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.4.0/css/all.min.css" integrity="sha256-HtsXJanqjKTc8vVQjO4YMhiqFoXkfBsjBWcX91T1jr8=" crossorigin="anonymous">
  <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/fancybox/3.5.7/jquery.fancybox.min.css" integrity="sha256-Vzbj7sDDS/woiFS3uNKo8eIuni59rjyNGtXfstRzStA=" crossorigin="anonymous">

<script class="next-config" data-name="main" type="application/json">{"hostname":"yanlwsometing.gitee.io","root":"/blog/","images":"/blog/images","scheme":"Pisces","darkmode":false,"version":"8.16.0","exturl":false,"sidebar":{"position":"left","display":"post","padding":18,"offset":12},"copycode":{"enable":true,"show_result":true,"style":"flat"},"bookmark":{"enable":false,"color":"#222","save":"auto"},"mediumzoom":false,"lazyload":false,"pangu":false,"comments":{"style":"tabs","active":null,"storage":true,"lazyload":false,"nav":null},"stickytabs":false,"motion":{"enable":false,"async":false,"transition":{"menu_item":"fadeInDown","post_block":"fadeIn","post_header":"fadeInDown","post_body":"fadeInDown","coll_header":"fadeInLeft","sidebar":"fadeInUp"}},"prism":false,"i18n":{"placeholder":"搜索...","empty":"没有找到任何搜索结果：${query}","hits_time":"找到 ${hits} 个搜索结果（用时 ${time} 毫秒）","hits":"找到 ${hits} 个搜索结果"}}</script><script src="/blog/js/config.js"></script>

    <meta name="description" content="apply策略当遇到如下场景时，采用apply策略：  待证目标与上下文中的前提或已证引理*’刚好相同’*的情况 123Theorem silly1 : forall (n m : nat),  n &#x3D; m -&gt; n &#x3D; m.Proof. intros n m eq. apply eq.  Qed.  待证目标存在于一个蕴含式中，就可以配合*’条件（Conditional）’*假设和引理来使">
<meta property="og:type" content="article">
<meta property="og:title" content="SF-1-Tactics">
<meta property="og:url" content="https://yanlwsometing.gitee.io/blog/2023/07/19/SF-1-Tactics/index.html">
<meta property="og:site_name" content="yanlwsometing">
<meta property="og:description" content="apply策略当遇到如下场景时，采用apply策略：  待证目标与上下文中的前提或已证引理*’刚好相同’*的情况 123Theorem silly1 : forall (n m : nat),  n &#x3D; m -&gt; n &#x3D; m.Proof. intros n m eq. apply eq.  Qed.  待证目标存在于一个蕴含式中，就可以配合*’条件（Conditional）’*假设和引理来使">
<meta property="og:locale" content="zh_CN">
<meta property="og:image" content="https://yanlwsometing.gitee.io/blog/images/SF-1-Tactics/image-20230729173954657.png">
<meta property="og:image" content="https://yanlwsometing.gitee.io/blog/images/SF-1-Tactics/image-20230729174106381.png">
<meta property="article:published_time" content="2023-07-19T09:19:31.000Z">
<meta property="article:modified_time" content="2023-12-15T09:08:43.930Z">
<meta property="article:author" content="yanlw">
<meta property="article:tag" content="博客">
<meta name="twitter:card" content="summary">
<meta name="twitter:image" content="https://yanlwsometing.gitee.io/blog/images/SF-1-Tactics/image-20230729173954657.png">


<link rel="canonical" href="https://yanlwsometing.gitee.io/blog/2023/07/19/SF-1-Tactics/">



<script class="next-config" data-name="page" type="application/json">{"sidebar":"","isHome":false,"isPost":true,"lang":"zh-CN","comments":true,"permalink":"https://yanlwsometing.gitee.io/blog/2023/07/19/SF-1-Tactics/","path":"2023/07/19/SF-1-Tactics/","title":"SF-1-Tactics"}</script>

<script class="next-config" data-name="calendar" type="application/json">""</script>
<title>SF-1-Tactics | yanlwsometing</title>
  








  <noscript>
    <link rel="stylesheet" href="/blog/css/noscript.css">
  </noscript>
</head>

<body itemscope itemtype="http://schema.org/WebPage">
  <div class="headband"></div>

  <main class="main">
    <div class="column">
      <header class="header" itemscope itemtype="http://schema.org/WPHeader"><div class="site-brand-container">
  <div class="site-nav-toggle">
    <div class="toggle" aria-label="切换导航栏" role="button">
        <span class="toggle-line"></span>
        <span class="toggle-line"></span>
        <span class="toggle-line"></span>
    </div>
  </div>

  <div class="site-meta">

    <a href="/blog/" class="brand" rel="start">
      <i class="logo-line"></i>
      <p class="site-title">yanlwsometing</p>
      <i class="logo-line"></i>
    </a>
  </div>

  <div class="site-nav-right">
    <div class="toggle popup-trigger" aria-label="搜索" role="button">
    </div>
  </div>
</div>



<nav class="site-nav">
  <ul class="main-menu menu"><li class="menu-item menu-item-home"><a href="/blog/" rel="section"><i class="fa fa-home fa-fw"></i>首页</a></li><li class="menu-item menu-item-tags"><a href="/blog/tags/" rel="section"><i class="fa fa-tags fa-fw"></i>标签</a></li><li class="menu-item menu-item-categories"><a href="/blog/categories/" rel="section"><i class="fa fa-th fa-fw"></i>分类</a></li><li class="menu-item menu-item-archives"><a href="/blog/archives/" rel="section"><i class="fa fa-archive fa-fw"></i>归档</a></li><li class="menu-item menu-item-commonweal"><a href="/blog/404/" rel="section"><i class="fa fa-heartbeat fa-fw"></i>公益 404</a></li>
  </ul>
</nav>




</header>
        
  
  <aside class="sidebar">

    <div class="sidebar-inner sidebar-nav-active sidebar-toc-active">
      <ul class="sidebar-nav">
        <li class="sidebar-nav-toc">
          文章目录
        </li>
        <li class="sidebar-nav-overview">
          站点概览
        </li>
      </ul>

      <div class="sidebar-panel-container">
        <!--noindex-->
        <div class="post-toc-wrap sidebar-panel">
            <div class="post-toc animated"><ol class="nav"><li class="nav-item nav-level-2"><a class="nav-link" href="#apply%E7%AD%96%E7%95%A5"><span class="nav-number">1.</span> <span class="nav-text">apply策略</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#apply-with-%E7%AD%96%E7%95%A5"><span class="nav-number">2.</span> <span class="nav-text">apply with 策略</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#The-injection-and-discriminate-Tactics"><span class="nav-number">3.</span> <span class="nav-text">The injection and discriminate Tactics</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#%E5%AF%B9%E5%81%87%E8%AE%BE%E4%BD%BF%E7%94%A8%E7%AD%96%E7%95%A5"><span class="nav-number">4.</span> <span class="nav-text">对假设使用策略</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#%E5%8F%98%E6%8D%A2%E5%BD%92%E7%BA%B3%E5%81%87%E8%AE%BE"><span class="nav-number">5.</span> <span class="nav-text">变换归纳假设</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#%E5%B1%95%E5%BC%80%E5%AE%9A%E4%B9%89"><span class="nav-number">6.</span> <span class="nav-text">展开定义</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#%E5%AF%B9%E5%A4%8D%E5%90%88%E8%A1%A8%E8%BE%BE%E5%BC%8F%E4%BD%BF%E7%94%A8-destruct"><span class="nav-number">7.</span> <span class="nav-text">对复合表达式使用 destruct</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#%E5%A4%8D%E4%B9%A0"><span class="nav-number">8.</span> <span class="nav-text">复习</span></a></li></ol></div>
        </div>
        <!--/noindex-->

        <div class="site-overview-wrap sidebar-panel">
          <div class="site-author animated" itemprop="author" itemscope itemtype="http://schema.org/Person">
    <img class="site-author-image" itemprop="image" alt="yanlw"
      src="/blog/images/avatar.jpg">
  <p class="site-author-name" itemprop="name">yanlw</p>
  <div class="site-description" itemprop="description">穷则独善其身，达则兼济天下！</div>
</div>
<div class="site-state-wrap animated">
  <nav class="site-state">
      <div class="site-state-item site-state-posts">
        <a href="/blog/archives/">
          <span class="site-state-item-count">23</span>
          <span class="site-state-item-name">日志</span>
        </a>
      </div>
      <div class="site-state-item site-state-categories">
          <a href="/blog/categories/">
        <span class="site-state-item-count">9</span>
        <span class="site-state-item-name">分类</span></a>
      </div>
      <div class="site-state-item site-state-tags">
          <a href="/blog/tags/">
        <span class="site-state-item-count">18</span>
        <span class="site-state-item-name">标签</span></a>
      </div>
  </nav>
</div>
  <div class="links-of-author animated">
      <span class="links-of-author-item">
        <a href="https://gitee.com/yanlwsometing" title="Gitee → https:&#x2F;&#x2F;gitee.com&#x2F;yanlwsometing" rel="noopener me" target="_blank"><i class="fab fa-gitee fa-fw"></i>Gitee</a>
      </span>
      <span class="links-of-author-item">
        <a href="mailto:1977712019@qq.com" title="Mail → mailto:1977712019@qq.com" rel="noopener me" target="_blank"><i class="fa fa-envelope fa-fw"></i>Mail</a>
      </span>
      <span class="links-of-author-item">
        <a href="https://weibo.com/" title="Weibo → https:&#x2F;&#x2F;weibo.com&#x2F;" rel="noopener me" target="_blank"><i class="fab fa-weibo fa-fw"></i>Weibo</a>
      </span>
      <span class="links-of-author-item">
        <a href="https://twitter.com/" title="Twitter → https:&#x2F;&#x2F;twitter.com&#x2F;" rel="noopener me" target="_blank"><i class="fab fa-twitter fa-fw"></i>Twitter</a>
      </span>
  </div>

        </div>
      </div>
        <div class="back-to-top animated" role="button" aria-label="返回顶部">
          <i class="fa fa-arrow-up"></i>
          <span>0%</span>
        </div>
    </div>

    
  </aside>


    </div>

    <div class="main-inner post posts-expand">


  


<div class="post-block">
  
  

  <article itemscope itemtype="http://schema.org/Article" class="post-content" lang="zh-CN">
    <link itemprop="mainEntityOfPage" href="https://yanlwsometing.gitee.io/blog/2023/07/19/SF-1-Tactics/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/blog/images/avatar.jpg">
      <meta itemprop="name" content="yanlw">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yanlwsometing">
      <meta itemprop="description" content="穷则独善其身，达则兼济天下！">
    </span>

    <span hidden itemprop="post" itemscope itemtype="http://schema.org/CreativeWork">
      <meta itemprop="name" content="SF-1-Tactics | yanlwsometing">
      <meta itemprop="description" content="">
    </span>
      <header class="post-header">
        <h1 class="post-title" itemprop="name headline">
          SF-1-Tactics
        </h1>

        <div class="post-meta-container">
          <div class="post-meta">
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar"></i>
      </span>
      <span class="post-meta-item-text">发表于</span>

      <time title="创建时间：2023-07-19 17:19:31" itemprop="dateCreated datePublished" datetime="2023-07-19T17:19:31+08:00">2023-07-19</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar-check"></i>
      </span>
      <span class="post-meta-item-text">更新于</span>
      <time title="修改时间：2023-12-15 17:08:43" itemprop="dateModified" datetime="2023-12-15T17:08:43+08:00">2023-12-15</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-folder"></i>
      </span>
      <span class="post-meta-item-text">分类于</span>
        <span itemprop="about" itemscope itemtype="http://schema.org/Thing">
          <a href="/blog/categories/Coq/" itemprop="url" rel="index"><span itemprop="name">Coq</span></a>
        </span>
    </span>

  
    <span class="post-meta-item" title="阅读次数" id="busuanzi_container_page_pv">
      <span class="post-meta-item-icon">
        <i class="far fa-eye"></i>
      </span>
      <span class="post-meta-item-text">阅读次数：</span>
      <span id="busuanzi_value_page_pv"></span>
    </span>
</div>

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody"><h2 id="apply策略"><a href="#apply策略" class="headerlink" title="apply策略"></a>apply策略</h2><p>当遇到如下场景时，采用apply策略：</p>
<ul>
<li><p>待证目标与上下文中的前提或已证引理*’刚好相同’*的情况</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br></pre></td><td class="code"><pre><span class="line">Theorem silly1 : forall (n m : nat),</span><br><span class="line">  n = m -&gt; n = m.</span><br><span class="line">Proof. intros n m eq. apply eq.  Qed.</span><br></pre></td></tr></table></figure>
</li>
<li><p>待证目标存在于一个蕴含式中，就可以配合*’条件（Conditional）’*假设和引理来使用，该蕴含式的前提就会被添加到待证子目标列表中</p>
</li>
<li><p>当我们使用 apply H 时，语句 H 会以一个引入了某些 <em>‘通用变量（Universal Variables）’</em> 的 ∀ 开始。在 Coq 针对 H 的结论匹配当前目标时，它会尝试为这些变量查找适当的值</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br></pre></td><td class="code"><pre><span class="line">Theorem silly2a : forall (n m : nat),</span><br><span class="line">  (n,n) = (m,m)  -&gt;</span><br><span class="line">  (forall (q r : nat), (q,q) = (r,r) -&gt; [q] = [r]) -&gt;</span><br><span class="line">  [n] = [m].</span><br><span class="line">Proof.</span><br><span class="line">  intros n m eq1 eq2.</span><br><span class="line">  apply eq2. apply eq1.  Qed.</span><br><span class="line"></span><br></pre></td></tr></table></figure>

<p>变量 q 匹配n ，而 r 匹配m </p>
</li>
<li><p>要使用 apply 策略，被应用的事实（的结论）必须精确地匹配证明目标： 例如, 当等式的左右两边互换后，apply 就无法起效了，这个时候需要采用<strong>symmetry</strong></p>
</li>
</ul>
<span id="more"></span>

<h2 id="apply-with-策略"><a href="#apply-with-策略" class="headerlink" title="apply with 策略"></a>apply with 策略</h2><p>在Coq中，<code>apply</code>策略用于应用一个已证明的引理或定理到当前的目标上。而<code>with</code>关键字则用于给定引理或定理应用的参数。<code>apply with</code>结合起来使用可以在应用引理时指定参数的值。</p>
<p>使用<code>apply with</code>的一般形式如下所示：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br></pre></td><td class="code"><pre><span class="line">apply lemma_name with (arg1 := val1) (arg2 := val2) ...)</span><br></pre></td></tr></table></figure>
<p>其中，<code>lemma_name</code>是待应用的引理或定理的名称，<code>arg1</code>, <code>arg2</code>, … 是引理或定理中参数的名称，<code>val1</code>, <code>val2</code>, … 是给定参数的值。</p>
<p>下面是一个简单的例子，展示了<code>apply with</code>的使用方式：</p>
<figure class="highlight coq"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br></pre></td><td class="code"><pre><span class="line"><span class="keyword">Lemma</span> add_comm : <span class="keyword">forall</span> n m : nat, n + m = m + n.</span><br><span class="line"><span class="keyword">Proof</span>.</span><br><span class="line">  <span class="built_in">intros</span> n m， <span class="comment">(* 证明... *)</span></span><br><span class="line"><span class="keyword">Qed</span>.</span><br><span class="line"></span><br><span class="line"><span class="keyword">Lemma</span> example : <span class="number">2</span> + <span class="number">3</span> = <span class="number">3</span> + <span class="number">2.</span></span><br><span class="line"><span class="keyword">Proof</span>.</span><br><span class="line">  <span class="built_in">apply</span> add_comm <span class="built_in">with</span> (n := <span class="number">2</span>) (m := <span class="number">3</span>).</span><br><span class="line"><span class="keyword">Qed</span>.</span><br></pre></td></tr></table></figure>

<p>在这个例子中，我们使用 <code>apply with</code> 在证明 <code>example</code> 中应用 <code>add_comm</code> 引理时指定了参数的具体值 <code>(n := 2)</code> 和 <code>(m := 3)</code>。</p>
<h2 id="The-injection-and-discriminate-Tactics"><a href="#The-injection-and-discriminate-Tactics" class="headerlink" title="The injection and discriminate Tactics"></a>The injection and discriminate Tactics</h2><p>injection让 Coq 利用构造子的单射性来产生所有它能从 H 所推出的等式，每一个这样的等式都作为假设（本例中为 Hmn）被添加到上下文中。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br></pre></td><td class="code"><pre><span class="line">Theorem S_injective : forall (n m : nat),</span><br><span class="line">  S n = S m -&gt;</span><br><span class="line">  n = m.</span><br><span class="line">Proof.</span><br><span class="line">  intros n m H1. injection H as Hnm. apply Hnm.</span><br><span class="line">Qed.</span><br><span class="line"></span><br></pre></td></tr></table></figure>

<p>discriminate 则是利用不相交原则，即两个以不同构造子开始的元素(如O和S，或真和假)永远不可能相等。当假设存在这样的荒谬性时，一切结论皆可证真。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br></pre></td><td class="code"><pre><span class="line">Theorem discriminate_ex1 : forall (n : nat),</span><br><span class="line">  S n = O -&gt; 2 + 2 = 5.</span><br><span class="line">Proof.</span><br><span class="line">  intros n contra. discriminate contra. Qed</span><br></pre></td></tr></table></figure>

<p>本例是逻辑学原理爆炸原理的一个实例，它断言矛盾的前提会推出任何东西， 甚至是假命题！</p>
<h2 id="对假设使用策略"><a href="#对假设使用策略" class="headerlink" title="对假设使用策略"></a>对假设使用策略</h2><ul>
<li><p>simpl in H 会对上下文中的假设 H 执行化简</p>
</li>
<li><p>apply L in H 会针对上下文中的假设 H 匹配某些 （形如 X → Y 中的）条件语句 L。然而，与一般的 apply 不同 （它将匹配 Y 的目标改写为子目标 X），apply L in H 会针对 X 匹配 H，如果成功，就将其替换为 Y</p>
<p>换言之，apply L in H 给了我们一种“正向推理”的方式：根据 X → Y 和一个匹配 X 的假设，它会产生一个匹配 Y 的假设。作为对比，apply L 是一种“反向推理”：它表示如果我们知道 X → Y 并且试图证明 Y， 那么证明 X 就足够了。</p>
</li>
</ul>
<h2 id="变换归纳假设"><a href="#变换归纳假设" class="headerlink" title="变换归纳假设"></a>变换归纳假设</h2><p>在调用 induction 策略前，我们有时需要用 intros 将假设从目标移到上下文中时要十分小心。例如，假设我们要证明 double 函数是单射的 </p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br><span class="line">14</span><br><span class="line">15</span><br><span class="line">16</span><br><span class="line">17</span><br><span class="line">18</span><br><span class="line">19</span><br></pre></td><td class="code"><pre><span class="line">Fixpoint double (n:nat) :=</span><br><span class="line">  match n with</span><br><span class="line">  | O =&gt; O</span><br><span class="line">  | S n&#x27; =&gt; S (S (double n&#x27;))</span><br><span class="line">  end.</span><br><span class="line"> </span><br><span class="line">Theorem double_injective_FAILED : forall n m,</span><br><span class="line">  double n = double m -&gt;</span><br><span class="line">  n = m.</span><br><span class="line">Proof.</span><br><span class="line">  intros n m. induction n as [| n&#x27; IHn&#x27;].</span><br><span class="line">  - (* n = O *) simpl. intros eq. destruct m as [| m&#x27;] eqn:E.</span><br><span class="line">    + (* m = O *) reflexivity.</span><br><span class="line">    + (* m = S m&#x27; *) discriminate eq.</span><br><span class="line">  - (* n = S n&#x27; *) intros eq. destruct m as [| m&#x27;] eqn:E.</span><br><span class="line">    + (* m = O *) discriminate eq.</span><br><span class="line">    + (* m = S m&#x27; *) apply f_equal.</span><br><span class="line"></span><br><span class="line">Abort.</span><br></pre></td></tr></table></figure>

<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br><span class="line">14</span><br><span class="line">15</span><br><span class="line">16</span><br><span class="line">17</span><br><span class="line">18</span><br><span class="line">19</span><br><span class="line">20</span><br><span class="line">21</span><br><span class="line">22</span><br><span class="line">23</span><br><span class="line">24</span><br><span class="line">25</span><br><span class="line">26</span><br><span class="line">27</span><br><span class="line">28</span><br><span class="line">29</span><br><span class="line">30</span><br><span class="line">31</span><br><span class="line">32</span><br><span class="line">33</span><br><span class="line">34</span><br><span class="line">35</span><br><span class="line">36</span><br><span class="line">37</span><br><span class="line">38</span><br><span class="line">39</span><br><span class="line">40</span><br><span class="line">41</span><br></pre></td><td class="code"><pre><span class="line">Theorem double_injective : forall n m,</span><br><span class="line">  double n = double m -&gt;</span><br><span class="line">  n = m.</span><br><span class="line">Proof.</span><br><span class="line">  intros n. induction n as [| n&#x27; IHn&#x27;].</span><br><span class="line">  - (* n = O *) simpl. intros m eq. destruct m as [| m&#x27;] eqn:E.</span><br><span class="line">    + (* m = O *) reflexivity.</span><br><span class="line">    + (* m = S m&#x27; *) discriminate eq.</span><br><span class="line"></span><br><span class="line">  - (* n = S n&#x27; *)</span><br><span class="line"></span><br><span class="line">(** Notice that both the goal and the induction hypothesis are</span><br><span class="line">    different this time: the goal asks us to prove something more</span><br><span class="line">    general (i.e., we must prove the statement for _every_ [m]), but</span><br><span class="line">    the IH is correspondingly more flexible, allowing us to choose any</span><br><span class="line">    [m] we like when we apply the IH. *)</span><br><span class="line"></span><br><span class="line">    intros m eq.</span><br><span class="line"></span><br><span class="line">(** Now we&#x27;ve chosen a particular [m] and introduced the assumption</span><br><span class="line">    that [double n = double m].  Since we are doing a case analysis on</span><br><span class="line">    [n], we also need a case analysis on [m] to keep the two &quot;in sync.&quot; *)</span><br><span class="line"></span><br><span class="line">    destruct m as [| m&#x27;] eqn:E.</span><br><span class="line">    + (* m = O *)</span><br><span class="line"></span><br><span class="line">(** The 0 case is trivial: *)</span><br><span class="line"></span><br><span class="line">    discriminate eq.</span><br><span class="line">    + (* m = S m&#x27; *)</span><br><span class="line">      apply f_equal.</span><br><span class="line"></span><br><span class="line">(** At this point, since we are in the second branch of the [destruct</span><br><span class="line">    m], the [m&#x27;] mentioned in the context is the predecessor of the</span><br><span class="line">    [m] we started out talking about.  Since we are also in the [S]</span><br><span class="line">    branch of the induction, this is perfect: if we instantiate the</span><br><span class="line">    generic [m] in the IH with the current [m&#x27;] (this instantiation is</span><br><span class="line">    performed automatically by the [apply] in the next step), then</span><br><span class="line">    [IHn&#x27;] gives us exactly what we need to finish the proof. *)</span><br><span class="line"></span><br><span class="line">      apply IHn&#x27;. simpl in eq. injection eq as goal. apply goal. Qed.</span><br></pre></td></tr></table></figure>



<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br><span class="line">14</span><br><span class="line">15</span><br><span class="line">16</span><br><span class="line">17</span><br><span class="line">18</span><br></pre></td><td class="code"><pre><span class="line">Theorem double_injective_take2 : forall n m,</span><br><span class="line">  double n = double m -&gt;</span><br><span class="line">  n = m.</span><br><span class="line">Proof.</span><br><span class="line">  intros n m.</span><br><span class="line">  (* [n] and [m] are both in the context *)</span><br><span class="line">  generalize dependent n.</span><br><span class="line">  (* Now [n] is back in the goal and we can do induction on</span><br><span class="line">     [m] and get a sufficiently general IH. *)</span><br><span class="line">  induction m as [| m&#x27; IHm&#x27;].</span><br><span class="line">  - (* m = O *) simpl. intros n eq. destruct n as [| n&#x27;] eqn:E.</span><br><span class="line">    + (* n = O *) reflexivity.</span><br><span class="line">    + (* n = S n&#x27; *) discriminate eq.</span><br><span class="line">  - (* m = S m&#x27; *) intros n eq. destruct n as [| n&#x27;] eqn:E.</span><br><span class="line">    + (* n = O *) discriminate eq.</span><br><span class="line">    + (* n = S n&#x27; *) apply f_equal.</span><br><span class="line">      apply IHm&#x27;. injection eq as goal. apply goal.</span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>

<p>先引入所有量化的变量，然后*’重新一般化（re-generalize）’* 其中的一个或几个，选择性地从上下文中挑出几个变量并将它们放回证明目标的开始处。 用 generalize dependent 策略就能做到。</p>
<p><strong>个人理解1</strong>：问题在于，对于<code>intros n , m, eq</code>, <code>eq</code>的非形式化含义为“任意的n和m, double n &#x3D; double m”。在<code>intros n. ..... intros m eq</code>， <code>eq</code>的非形式化含义为“对于任意的n，有m（任意但具体）使double n &#x3D; double m”。因此，需要延后m的引入时间。</p>
<p><strong>个人理解2</strong>：先看对比图</p>
<p><img src="/blog/images/SF-1-Tactics/image-20230729173954657.png" alt="image-20230729173954657"></p>
<p><img src="/blog/images/SF-1-Tactics/image-20230729174106381.png" alt="image-20230729174106381"></p>
<p>在不同位置引入假设，归纳前提结论是不同的，因此图一我们理所应当地认为只要<code>apply IHm&#39;</code>, 就能顺利证明成功，但是Coq不会这么做。</p>
<p>因为<code>IHm&#39;</code>的性质不同，图一的是作为事实陈述的，它的背景含义是（n和m已经确定了）；而图二是作为命题结论的，它的背景含义是任意但确定的n</p>
<p>因此什么时候变换归纳假设，就是在出现像图一那样，看上去假设可用但又用不了的情况。</p>
<h2 id="展开定义"><a href="#展开定义" class="headerlink" title="展开定义"></a>展开定义</h2><p><code>unfold</code> 是一个替换操作，用于展开（或展开定义）标识符（变量、函数、定理等）。它的主要作用是将标识符替换为其定义，从而在证明过程中更好地观察和操作项。</p>
<p><code>unfold</code> 有两种使用方式：</p>
<ol>
<li>展开单个标识符：可以使用 <code>unfold &lt;identifier&gt;</code> 来展开某个具体的标识符。例如，如果有一个变量 <code>x</code>，你可以使用 <code>unfold x</code> 来将所有出现的 <code>x</code> 替换为其具体的值或定义。</li>
<li>展开多个标识符：如果你想同时展开多个标识符，可以使用 <code>unfold &lt;identifier1&gt;, &lt;identifier2&gt;, ...</code> 的形式。例如，<code>unfold f, g</code> 将展开标识符 <code>f</code> 和 <code>g</code>。</li>
</ol>
<p>这个指令在证明过程中非常有用，特别是在展开定义或简化复杂的表达式时。通过展开，你可以更加清晰地了解项和其定义之间的关系，并且可以更方便地进行后续的推理和证明。</p>
<h2 id="对复合表达式使用-destruct"><a href="#对复合表达式使用-destruct" class="headerlink" title="对复合表达式使用 destruct"></a>对复合表达式使用 destruct</h2><p>destruct 可以进行分类来处理一些变量的值了，也可以根据某些*’表达式’*的结果的情况来进行推理。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br><span class="line">14</span><br></pre></td><td class="code"><pre><span class="line">Definition sillyfun (n : nat) : bool :=</span><br><span class="line">  if n =? 3 then false</span><br><span class="line">  else if n =? 5 then false</span><br><span class="line">  else false.</span><br><span class="line">Theorem sillyfun_false : forall (n : nat),</span><br><span class="line">  sillyfun n = false.</span><br><span class="line">Proof.</span><br><span class="line">  intros n. unfold sillyfun.</span><br><span class="line">  destruct (n =? 3) eqn:E1.</span><br><span class="line">    - (* n =? 3 = true *) reflexivity.</span><br><span class="line">    - (* n =? 3 = false *) destruct (n =? 5) eqn:E2.</span><br><span class="line">      + (* n =? 5 = true *) reflexivity.</span><br><span class="line">      + (* n =? 5 = false *) reflexivity. </span><br><span class="line">Qed.</span><br></pre></td></tr></table></figure>

<p>由于 n 要么等于 3 要么不等于，因此我们可以用 destruct (eqb n 3) 来对这两种情况进行推理</p>
<h2 id="复习"><a href="#复习" class="headerlink" title="复习"></a>复习</h2><ul>
<li>intros：将前提&#x2F;变量从证明目标移到上下文中</li>
<li>reflexivity：（当目标形如 e &#x3D; e 时）结束证明</li>
<li>apply：用前提、引理或构造子证明目标</li>
<li>apply… in H：将前提、引理或构造子应用到上下文中的假设上（正向推理）</li>
<li>apply… with…：为无法被模式匹配确定的变量显式指定</li>
<li>simpl：化简目标中的计算</li>
<li>simpl in H：化简前提中的计算</li>
<li>rewrite：使用相等关系假设（或引理）来改写目标</li>
<li>rewrite … in H：使用相等关系假设（或引理）来改写前提</li>
<li>symmetry：将形如 t&#x3D;u 的目标改为 u&#x3D;t</li>
<li>symmetry in H：将形如 t&#x3D;u 的前提改为 u&#x3D;t</li>
<li>unfold：用目标中的右式替换定义的常量</li>
<li>unfold… in H：用前提中的右式替换定义的常量</li>
<li>destruct… as…：对归纳定义类型的值进行情况分析</li>
<li>destruct… eqn:…：为添加到上下文中的等式指定名字， 记录情况分析的结果</li>
<li>induction… as…: 对归纳定义类型的值进行归纳</li>
<li>injection: reason by injectivity on equalities between values of inductively defined types</li>
<li>discriminate: reason by disjointness of constructors on equalities between values of inductively defined types</li>
<li>assert (H: e)（或 assert (e) as H）：引入“局部引理”e 并称之为 H</li>
<li>generalize dependent x：将变量 x（以及任何依赖它的东西） 从上下文中移回目标公式内的前提中</li>
</ul>

    </div>

    
    
    

    <footer class="post-footer">

        

          <div class="post-nav">
            <div class="post-nav-item">
                <a href="/blog/2023/07/19/SF-1-Poly/" rel="prev" title="SF-1-Poly">
                  <i class="fa fa-chevron-left"></i> SF-1-Poly
                </a>
            </div>
            <div class="post-nav-item">
                <a href="/blog/2023/07/22/SF-1-Logic/" rel="next" title="SF-1-Logic">
                  SF-1-Logic <i class="fa fa-chevron-right"></i>
                </a>
            </div>
          </div>
    </footer>
  </article>
</div>






</div>
  </main>

  <footer class="footer">
    <div class="footer-inner">


<div class="copyright">
  &copy; 
  <span itemprop="copyrightYear">2023</span>
  <span class="with-love">
    <i class="fa fa-heart"></i>
  </span>
  <span class="author" itemprop="copyrightHolder">yanlw</span>
</div>
<div class="busuanzi-count">
    <span class="post-meta-item" id="busuanzi_container_site_uv">
      <span class="post-meta-item-icon">
        <i class="fa fa-user"></i>
      </span>
      <span class="site-uv" title="总访客量">
        <span id="busuanzi_value_site_uv"></span>
      </span>
    </span>
    <span class="post-meta-item" id="busuanzi_container_site_pv">
      <span class="post-meta-item-icon">
        <i class="fa fa-eye"></i>
      </span>
      <span class="site-pv" title="总访问量">
        <span id="busuanzi_value_site_pv"></span>
      </span>
    </span>
</div>
  <div class="powered-by">由 <a href="https://hexo.io/" rel="noopener" target="_blank">Hexo</a> & <a href="https://theme-next.js.org/pisces/" rel="noopener" target="_blank">NexT.Pisces</a> 强力驱动
  </div>

    </div>
  </footer>

  
  <div class="reading-progress-bar"></div>

  <a href="https://gitee.com/yanlwsometing" class="github-corner" title="在 GitHub 上关注我" aria-label="在 GitHub 上关注我" rel="noopener" target="_blank"><svg width="80" height="80" viewBox="0 0 250 250" aria-hidden="true"><path d="M0,0 L115,115 L130,115 L142,142 L250,250 L250,0 Z"></path><path d="M128.3,109.0 C113.8,99.7 119.0,89.6 119.0,89.6 C122.0,82.7 120.5,78.6 120.5,78.6 C119.2,72.0 123.4,76.3 123.4,76.3 C127.3,80.9 125.5,87.3 125.5,87.3 C122.9,97.6 130.6,101.9 134.4,103.2" fill="currentColor" style="transform-origin: 130px 106px;" class="octo-arm"></path><path d="M115.0,115.0 C114.9,115.1 118.7,116.5 119.8,115.4 L133.7,101.6 C136.9,99.2 139.9,98.4 142.2,98.6 C133.8,88.0 127.5,74.4 143.8,58.0 C148.5,53.4 154.0,51.2 159.7,51.0 C160.3,49.4 163.2,43.6 171.4,40.1 C171.4,40.1 176.1,42.5 178.8,56.2 C183.1,58.6 187.2,61.8 190.9,65.4 C194.5,69.0 197.7,73.2 200.1,77.6 C213.8,80.2 216.3,84.9 216.3,84.9 C212.7,93.1 206.9,96.0 205.4,96.6 C205.1,102.4 203.0,107.8 198.3,112.5 C181.9,128.9 168.3,122.5 157.7,114.1 C157.9,116.9 156.7,120.9 152.7,124.9 L141.0,136.5 C139.8,137.7 141.6,141.9 141.8,141.8 Z" fill="currentColor" class="octo-body"></path></svg></a>

<noscript>
  <div class="noscript-warning">Theme NexT works best with JavaScript enabled</div>
</noscript>


  
  <script src="https://cdnjs.cloudflare.com/ajax/libs/animejs/3.2.1/anime.min.js" integrity="sha256-XL2inqUJaslATFnHdJOi9GfQ60on8Wx1C2H8DYiN1xY=" crossorigin="anonymous"></script>
  <script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.6.4/jquery.min.js" integrity="sha256-oP6HI9z1XaZNBrJURtCoUT5SUnxFr8s3BzRl+cbzUq8=" crossorigin="anonymous"></script>
  <script src="https://cdnjs.cloudflare.com/ajax/libs/fancybox/3.5.7/jquery.fancybox.min.js" integrity="sha256-yt2kYMy0w8AbtF89WXb2P1rfjcP/HTHLT7097U8Y5b8=" crossorigin="anonymous"></script>
<script src="/blog/js/comments.js"></script><script src="/blog/js/utils.js"></script><script src="/blog/js/next-boot.js"></script>

  


  <script src="/blog/js/third-party/fancybox.js"></script>



  
  <script async src="https://busuanzi.ibruce.info/busuanzi/2.3/busuanzi.pure.mini.js"></script>





</body>
</html>
